(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 81)) (_ BitVec 66))
(declare-fun p0 ( (_ BitVec 97) (_ BitVec 45)) Bool)
(declare-fun v0 () (_ BitVec 69))
(declare-fun v1 () (_ BitVec 109))
(assert (let ((e2(_ bv2872086227470285774622419 82)))
(let ((e3(_ bv3583338056299140152991285942269769 112)))
(let ((e4 (ite (= ((_ sign_extend 27) e2) v1) (_ bv1 1) (_ bv0 1))))
(let ((e5 (f0 ((_ extract 92 12) v1))))
(let ((e6 (bvshl ((_ sign_extend 43) e5) v1)))
(let ((e7 (ite (bvsle e3 ((_ sign_extend 111) e4)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (p0 ((_ extract 100 4) e6) ((_ extract 44 0) e2)) (_ bv1 1) (_ bv0 1))))
(let ((e9 (bvand ((_ zero_extend 65) e4) e5)))
(let ((e10 (bvcomp v1 ((_ sign_extend 108) e7))))
(let ((e11 (bvshl e3 ((_ sign_extend 111) e10))))
(let ((e12 (ite (bvuge v1 ((_ zero_extend 43) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvsrem ((_ zero_extend 111) e12) e3)))
(let ((e14 (bvsrem ((_ sign_extend 65) e12) e9)))
(let ((e15 (f0 ((_ extract 84 4) e11))))
(let ((e16 (bvsdiv ((_ sign_extend 43) v0) e13)))
(let ((e17 (= ((_ sign_extend 16) e9) e2)))
(let ((e18 (bvugt e6 ((_ sign_extend 43) e14))))
(let ((e19 (bvugt ((_ zero_extend 13) v0) e2)))
(let ((e20 (p0 ((_ zero_extend 96) e4) ((_ zero_extend 44) e7))))
(let ((e21 (bvslt e9 ((_ zero_extend 65) e4))))
(let ((e22 (bvsgt e5 ((_ zero_extend 65) e4))))
(let ((e23 (distinct ((_ sign_extend 43) e9) v1)))
(let ((e24 (bvule e11 ((_ zero_extend 46) e15))))
(let ((e25 (bvuge e13 ((_ sign_extend 111) e12))))
(let ((e26 (bvsle ((_ sign_extend 108) e7) e6)))
(let ((e27 (distinct ((_ zero_extend 46) e14) e11)))
(let ((e28 (bvule v0 ((_ sign_extend 68) e7))))
(let ((e29 (distinct ((_ sign_extend 43) e15) e6)))
(let ((e30 (bvsle ((_ zero_extend 46) e14) e16)))
(let ((e31 (bvsle ((_ sign_extend 46) e14) e16)))
(let ((e32 (distinct e11 e13)))
(let ((e33 (bvsgt e5 ((_ sign_extend 65) e4))))
(let ((e34 (bvuge ((_ sign_extend 46) e15) e11)))
(let ((e35 (p0 ((_ extract 102 6) e6) ((_ extract 71 27) e6))))
(let ((e36 (bvslt e6 ((_ zero_extend 108) e10))))
(let ((e37 (bvugt ((_ zero_extend 111) e8) e11)))
(let ((e38 (= e2 ((_ sign_extend 81) e10))))
(let ((e39 (bvugt e6 ((_ zero_extend 108) e12))))
(let ((e40 (bvule e16 e13)))
(let ((e41 (bvult e5 ((_ zero_extend 65) e12))))
(let ((e42 (distinct ((_ sign_extend 65) e8) e14)))
(let ((e43 (bvslt e8 e4)))
(let ((e44 (p0 ((_ zero_extend 31) e9) ((_ extract 61 17) e15))))
(let ((e45 (bvult e8 e7)))
(let ((e46 (bvsle e16 ((_ sign_extend 111) e12))))
(let ((e47 (= ((_ sign_extend 43) e9) e6)))
(let ((e48 (bvsle e2 ((_ zero_extend 81) e7))))
(let ((e49 (bvule e5 ((_ sign_extend 65) e12))))
(let ((e50 (bvugt ((_ sign_extend 65) e4) e9)))
(let ((e51 (bvult e13 ((_ zero_extend 30) e2))))
(let ((e52 (bvsgt e15 ((_ zero_extend 65) e8))))
(let ((e53 (bvsge ((_ zero_extend 46) e5) e13)))
(let ((e54 (bvslt e8 e4)))
(let ((e55 (bvult e8 e8)))
(let ((e56 (bvsge e14 ((_ zero_extend 65) e7))))
(let ((e57 (p0 ((_ extract 109 13) e16) ((_ extract 51 7) e5))))
(let ((e58 (bvugt ((_ zero_extend 108) e10) v1)))
(let ((e59 (= e14 ((_ zero_extend 65) e7))))
(let ((e60 (bvugt ((_ zero_extend 108) e4) e6)))
(let ((e61 (bvule v1 ((_ zero_extend 108) e8))))
(let ((e62 (= v1 ((_ zero_extend 27) e2))))
(let ((e63 (bvslt v1 ((_ sign_extend 43) e5))))
(let ((e64 (bvslt ((_ zero_extend 68) e10) v0)))
(let ((e65 (bvsle e6 ((_ sign_extend 108) e10))))
(let ((e66 (bvugt ((_ sign_extend 46) e15) e3)))
(let ((e67 (or e44 e52)))
(let ((e68 (or e55 e59)))
(let ((e69 (= e29 e62)))
(let ((e70 (ite e28 e49 e32)))
(let ((e71 (= e18 e47)))
(let ((e72 (not e19)))
(let ((e73 (xor e53 e54)))
(let ((e74 (ite e72 e42 e69)))
(let ((e75 (and e26 e25)))
(let ((e76 (= e22 e65)))
(let ((e77 (not e75)))
(let ((e78 (=> e33 e21)))
(let ((e79 (and e56 e77)))
(let ((e80 (or e78 e31)))
(let ((e81 (xor e46 e37)))
(let ((e82 (not e74)))
(let ((e83 (or e20 e51)))
(let ((e84 (ite e61 e81 e30)))
(let ((e85 (not e39)))
(let ((e86 (or e84 e48)))
(let ((e87 (or e73 e76)))
(let ((e88 (=> e40 e40)))
(let ((e89 (and e60 e45)))
(let ((e90 (= e57 e82)))
(let ((e91 (xor e24 e34)))
(let ((e92 (=> e68 e27)))
(let ((e93 (= e64 e23)))
(let ((e94 (not e50)))
(let ((e95 (xor e43 e92)))
(let ((e96 (ite e83 e67 e87)))
(let ((e97 (ite e85 e79 e85)))
(let ((e98 (or e58 e58)))
(let ((e99 (xor e91 e93)))
(let ((e100 (xor e36 e94)))
(let ((e101 (or e100 e17)))
(let ((e102 (xor e88 e86)))
(let ((e103 (xor e102 e70)))
(let ((e104 (not e99)))
(let ((e105 (xor e104 e103)))
(let ((e106 (ite e96 e63 e63)))
(let ((e107 (=> e89 e98)))
(let ((e108 (ite e101 e95 e105)))
(let ((e109 (= e41 e97)))
(let ((e110 (xor e108 e71)))
(let ((e111 (=> e90 e66)))
(let ((e112 (xor e107 e106)))
(let ((e113 (ite e109 e112 e109)))
(let ((e114 (=> e80 e113)))
(let ((e115 (xor e111 e38)))
(let ((e116 (ite e35 e114 e115)))
(let ((e117 (and e110 e116)))
(let ((e118 (and e117 (not (= e3 (_ bv0 112))))))
(let ((e119 (and e118 (not (= e3 (bvnot (_ bv0 112)))))))
(let ((e120 (and e119 (not (= e9 (_ bv0 66))))))
(let ((e121 (and e120 (not (= e9 (bvnot (_ bv0 66)))))))
(let ((e122 (and e121 (not (= e13 (_ bv0 112))))))
(let ((e123 (and e122 (not (= e13 (bvnot (_ bv0 112)))))))
e123
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
